Search for: All records

Regular resolution is a refinement of the resolution proof system requiring that no variable be resolved on more than once along any path in the proof. It is known that there exist sequences of formulas that require exponential-size proofs in regular resolution while admitting polynomial-size proofs in resolution. Thus, with respect to the usual notion of simulation, regular resolution is separated from resolution. An alternative, and weaker, notion for comparing proof systems is that of an “effective simulation,” which allows the translation of the formula along with the proof when moving between proof systems. We prove that regular resolution is equivalent to resolution under effective simulations. As a corollary, we recover in a black-box fashion a recent result on the hardness of automating regular resolution. 

We study propositional proof systems with inference rules that formalize restricted versions of the ability to make assumptions that hold without loss of generality, commonly used informally to shorten proofs. Each system we study is built on resolution. They are called BC⁻, RAT⁻, SBC⁻, and GER⁻, denoting respectively blocked clauses, resolution asymmetric tautologies, set-blocked clauses, and generalized extended resolution - all without new variables. They may be viewed as weak versions of extended resolution (ER) since they are defined by first generalizing the extension rule and then taking away the ability to introduce new variables. Except for SBC⁻, they are known to be strictly between resolution and extended resolution. Several separations between these systems were proved earlier by exploiting the fact that they effectively simulate ER. We answer the questions left open: We prove exponential lower bounds for SBC⁻ proofs of a binary encoding of the pigeonhole principle, which separates ER from SBC⁻. Using this new separation, we prove that both RAT⁻ and GER⁻ are exponentially separated from SBC⁻. This completes the picture of their relative strengths. 

We study the complexity of proof systems augmenting resolution with inference rules that allow, given a formula Γ in conjunctive normal form, deriving clauses that are not necessarily logically implied by Γ but whose addition to Γ preserves satisfiability. When the derived clauses are allowed to introduce variables not occurring in Γ, the systems we consider become equivalent to extended resolution. We are concerned with the versions of these systems without new variables. They are called BC⁻, RAT⁻, SBC⁻, and GER⁻, denoting respectively blocked clauses, resolution asymmetric tautologies, set-blocked clauses, and generalized extended resolution. Each of these systems formalizes some restricted version of the ability to make assumptions that hold --- without loss of generality --- which is commonly used informally to simplify or shorten proofs. Except for SBC⁻, these systems are known to be exponentially weaker than extended resolution. They are, however, all equivalent to it under a relaxed notion of simulation that allows the translation of the formula along with the proof when moving between proof systems. By taking advantage of this fact, we construct formulas that separate RAT⁻ from GER⁻ and vice versa. With the same strategy, we also separate SBC⁻ from RAT⁻. Additionally, we give polynomial-size SBC⁻ proofs of the pigeonhole principle, which separates SBC⁻ from GER⁻ by a previously known lower bound. These results also separate the three systems from BC⁻ since they all simulate it. We thus give an almost complete picture of their relative strengths. 

Abstract We explore the Collatz conjecture and its variants through the lens of termination of string rewriting. We construct a rewriting system that simulates the iterated application of the Collatz function on strings corresponding to mixed binary–ternary representations of positive integers. We prove that the termination of this rewriting system is equivalent to the Collatz conjecture. We also prove that a previously studied rewriting system that simulates the Collatz function using unary representations does not admit termination proofs via natural matrix interpretations, even when used in conjunction with dependency pairs. To show the feasibility of our approach in proving mathematically interesting statements, we implement a minimal termination prover that uses natural/arctic matrix interpretations and we find automated proofs of nontrivial weakenings of the Collatz conjecture. Although we do not succeed in proving the Collatz conjecture, we believe that the ideas here represent an interesting new approach. 

We explore the Collatz conjecture and its variants through the lens of termination of string rewriting. We construct a rewriting system that simulates the iterated application of the Collatz function on strings corresponding to mixed binary–ternary representations of positive integers. Termination of this rewriting system is equivalent to the Collatz conjecture. To show the feasibility of our approach in proving mathematically interesting statements, we implement a minimal termination prover that uses the automated method of matrix/arctic interpretations and we perform experiments where we obtain proofs of nontrivial weakenings of the Collatz conjecture. Finally, we adapt our rewriting system to show that other open problems in mathematics can also be approached as termination problems for relatively small rewriting systems. Although we do not succeed in proving the Collatz conjecture, we believe that the ideas here represent an interesting new approach. 

Mycielski graphs are a family of triangle-free graphs 𝑀_𝑘 with arbitrarily high chromatic number. 𝑀_𝑘 has chromatic number k and there is a short informal proof of this fact, yet finding proofs of it via automated reasoning techniques has proved to be a challenging task. In this paper, we study the complexity of clausal proofs of the uncolorability of 𝑀_𝑘 with 𝑘−1 colors. In particular, we consider variants of the PR (propagation redundancy) proof system that are without new variables, and with or without deletion. These proof systems are of interest due to their potential uses for proof search. As our main result, we present a sublinear-length and constant-width PR proof without new variables or deletion. We also implement a proof generator and verify the correctness of our proof. Furthermore, we consider formulas extended with clauses from the proof until a short resolution proof exists, and investigate the performance of CDCL in finding the short proof. This turns out to be difficult for CDCL with the standard heuristics. Finally, we describe an approach inspired by SAT sweeping to find proofs of these extended formulas.